; <lemma>
;  <title>ch7_conc.13</title>
;  <origin>ch7_conc | conc_1 | INITIALISATION/inv9/INV</origin>
(benchmark ch7_conc_13
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;  </typenv>
  :extramacros (
		 (enum1 (lambda (?i1 Int) . (= ?i1 1)))
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 )
; <goal>{1} = 1 .. 1</goal>
  :formula
  (not
      (= enum1 (range 1 1))
    )
)
; </lemma>
